import Mathlib.Algebra.Group.Defs import Mathlib.Init.Algebra.Order import ECTate.Algebra.Ring.Basic import Mathlib.Init.Data.Nat.Lemmas import ECTate.Init.Data.Int.Lemmas import ECTate.Data.Nat.Enat import Mathlib.Init.Data.Int.Basic import ECTate.Algebra.EllipticCurve.Kronecker import Mathlib.Tactic.LibrarySearch import Mathlib.Tactic.Ring import Mathlib.Tactic.Convert --class ValueMonoid (A : Type u) extends AddCommMonoid A, LinearOrder A open Enat section Obvious lemmamatch_non_zero (x :x: ββͺβββͺβ) {ββͺβ: Typec1c1: Ξ²c2 :c2: Ξ²Ξ²} :Ξ²: ?m.5x βx: ββͺβ0 β (match0: ?m.18x with |x: ββͺβ0 =>0: ββͺβc1 | _ =>c1: Ξ²c2) =c2: Ξ²c2 :=c2: Ξ²Goals accomplished! πGoals accomplished! πtheorem nat_mul_left_cancel (Goals accomplished! πaa: βbb: βc :c: βNat) (Nat: Typeh :h: a β 0a βa: β0) :0: ?m.940a *a: βb =b: βa *a: βc βc: βb =b: βc := Nat.eq_of_mul_eq_mul_left (Nat.pos_of_ne_zeroc: βh) end Obvious structureh: a β 0SurjVal {SurjVal: {R : Type u} β R β [inst : IntegralDomain R] β Type uR :R: Type uType u} (Type u: Type (u + 1)p :p: RR) [R: Type uIntegralDomainIntegralDomain: Type ?u.1068 β Type ?u.1068R] whereR: Type uv :v: {R : Type u} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβR βR: Type uββͺβββͺβ: Typev_uniformizer :v_uniformizer: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : SurjVal p), SurjVal.v self p = ofN 1vv: R β ββͺβp = ofNp: R1 v_mul_eq_add_v (1: ?m.1079aa: Rb :b: RR) :R: Type uv (v: R β ββͺβa *a: Rb) =b: Rvv: R β ββͺβa +a: Rvv: R β ββͺβb v_add_ge_min_v (b: Raa: Rb :b: RR) :R: Type uv (v: R β ββͺβa +a: Rb) β₯b: Rmin (min: {Ξ± : Type ?u.1326} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±vv: R β ββͺβa) (a: Rvv: R β ββͺβb) v_eq_top_iff_zero (b: Ra :a: RR) :R: Type uvv: R β ββͺβa =a: Rβ ββ: ββͺβa =a: R0 variable {0: ?m.1352R :R: Type uType u} [Type u: Type (u + 1)IntegralDomainIntegralDomain: Type ?u.2056 β Type ?u.2056R] section SurjVal lemmaR: Type up_non_zero {p_non_zero: β {R : Type u} [inst : IntegralDomain R] {p : R}, SurjVal p β Β¬p = 0p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2061} β R β [inst : IntegralDomain R] β Type ?u.2061p) : Β¬p: Rp =p: R0 :=0: ?m.2071@[simp] lemma val_zero {Goals accomplished! πp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2231} β R β [inst : IntegralDomain R] β Type ?u.2231p) :p: Rnav.nav: SurjVal pvv: {R : Type ?u.2240} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβ0 =0: ?m.2248β := (β: ββͺβnav.v_eq_top_iff_zeronav: SurjVal p0).0: ?m.230822: β {a b : Prop}, (a β b) β b β arfl lemmarfl: β {Ξ± : Sort ?u.2314} {a : Ξ±}, a = aval_mul_ge_left {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2340} β R β [inst : IntegralDomain R] β Type ?u.2340p) (p: Raa: Rb :b: RR) :R: Type unav.nav: SurjVal pv (v: {R : Type ?u.2353} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rnav.nav: SurjVal pvv: {R : Type ?u.2453} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa := Enat.le_trans (le_add_right (a: Rnav.nav: SurjVal pvv: {R : Type ?u.2478} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa) (a: Rnav.nav: SurjVal pvv: {R : Type ?u.2482} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb)) (le_of_eq (b: Rnav.v_mul_eq_add_vnav: SurjVal paa: Rb).symm) lemmab: Rval_mul_ge_right {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2522} β R β [inst : IntegralDomain R] β Type ?u.2522p) (p: Raa: Rb :b: RR) :R: Type unav.nav: SurjVal pv (v: {R : Type ?u.2535} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rnav.nav: SurjVal pvv: {R : Type ?u.2635} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb :=b: RlemmaGoals accomplished! πval_mul_ge_of_left_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2786} β R β [inst : IntegralDomain R] β Type ?u.2786p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.2796} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rn) :n: ?m.2781nav.nav: SurjVal pv (v: {R : Type ?u.2808} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rn := Enat.le_trans ha (val_mul_ge_leftn: ?m.2781navnav: SurjVal paa: Rb) lemmab: Rval_mul_ge_of_right_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.2950} β R β [inst : IntegralDomain R] β Type ?u.2950p) {p: Raa: Rb :b: RR} (hb :R: Type unav.nav: SurjVal pvv: {R : Type ?u.2986} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.2971nav.nav: SurjVal pv (v: {R : Type ?u.2998} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rn := Enat.le_trans hb (val_mul_ge_rightn: ?m.2971navnav: SurjVal paa: Rb) lemmab: Rval_mul_ge_of_both_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.3198} β R β [inst : IntegralDomain R] β Type ?u.3198p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.3208} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rm) (hb :m: ?m.3161nav.nav: SurjVal pvv: {R : Type ?u.3217} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.3193nav.nav: SurjVal pv (v: {R : Type ?u.3226} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa *a: Rb) β₯b: Rm +m: ?m.3161n :=n: ?m.3193@[simp] lemma val_of_one {Goals accomplished! πp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.3442} β R β [inst : IntegralDomain R] β Type ?u.3442p) :p: Rnav.nav: SurjVal pvv: {R : Type ?u.3451} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβ1 = ofN1: ?m.34590 :=0: ?m.3511
alemmaGoals accomplished! πval_pow_ge_of_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.3719} β R β [inst : IntegralDomain R] β Type ?u.3719p) {p: Ra :a: RR} (R: Type uk :k: ββ) (ha :β: Typenav.nav: SurjVal pvv: {R : Type ?u.3755} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rm) :m: ?m.3740nav.nav: SurjVal pv (v: {R : Type ?u.3767} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa ^a: Rk) β₯k: βk β’k: βm :=m: ?m.3740Goals accomplished! πlemmaGoals accomplished! πval_add_ge_of_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.4790} β R β [inst : IntegralDomain R] β Type ?u.4790p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.4800} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rn) (hb :n: ?m.4785nav.nav: SurjVal pvv: {R : Type ?u.4812} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.4785nav.nav: SurjVal pv (v: {R : Type ?u.4821} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa +a: Rb) β₯b: Rn := Enat.le_trans (n: ?m.4785le_min ha hb) (le_min: β {Ξ± : Type ?u.4946} [inst : LinearOrder Ξ±] {a b c : Ξ±}, c β€ a β c β€ b β c β€ min a bnav.v_add_ge_min_vnav: SurjVal paa: Rb) def nat_of_val {b: Rp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.4974} β R β [inst : IntegralDomain R] β Type ?u.4974p) {p: Ra :a: RR} (R: Type uh :h: a β 0a βa: R0) :0: ?m.4987β := to_nat ((not_iff_not.β: Type2 (2: β {a b : Prop}, (a β b) β b β anav.v_eq_top_iff_zeronav: SurjVal pa)).a: R22: β {a b : Prop}, (a β b) β b β ah) /- lemma val_of_add_one {p : R} (nav : SurjVal p) (h : nav.v x β₯ ofN 1): nav.v (x + 1) = ofN 0 := by apply Enat.le_antisymm . apply le_of_not_lt intro h' sorry . apply Enat.le_trans _ (nav.v_add_ge_min_v x 1) apply le_min (Enat.le_trans (Enat.le_succ 0) h) (le_of_eq (val_of_one nav).symm) -/ @[simp] lemmah: a β 0val_of_minus_one {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.5146} β R β [inst : IntegralDomain R] β Type ?u.5146p) :p: Rnav.nav: SurjVal pv (-v: {R : Type ?u.5155} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβ1) = ofN1: ?m.51640 :=0: ?m.5247Goals accomplished! πGoals accomplished! π@[simp] lemma val_neg {Goals accomplished! πp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.5788} β R β [inst : IntegralDomain R] β Type ?u.5788p) :p: Rnav.nav: SurjVal pv (-v: {R : Type ?u.5817} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx) =x: ?m.5806nav.nav: SurjVal pvv: {R : Type ?u.5845} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx :=x: ?m.5806lemmaGoals accomplished! πval_sub_ge_of_ge {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.6115} β R β [inst : IntegralDomain R] β Type ?u.6115p) {p: Raa: Rb :b: RR} (ha :R: Type unav.nav: SurjVal pvv: {R : Type ?u.6125} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa β₯a: Rn) (hb :n: ?m.6110nav.nav: SurjVal pvv: {R : Type ?u.6137} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb β₯b: Rn) :n: ?m.6110nav.nav: SurjVal pv (v: {R : Type ?u.6146} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa -a: Rb) β₯b: Rn :=n: ?m.6110theoremGoals accomplished! πv_add_eq_min_v {p :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.6665} β R β [inst : IntegralDomain R] β Type ?u.6665p) {p: Raa: Rb :b: RR} (h :R: Type unav.nav: SurjVal pvv: {R : Type ?u.6678} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa <a: Rnav.nav: SurjVal pvv: {R : Type ?u.6685} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb) :b: Rnav.nav: SurjVal pv (v: {R : Type ?u.6697} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa +a: Rb) =b: Rnav.nav: SurjVal pvv: {R : Type ?u.6798} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa :=a: RGoals accomplished! πGoals accomplished! πtheorem val_of_pow_uniformizer {Goals accomplished! πp :p: RR} (R: Type unav :nav: SurjVal pSurjValSurjVal: {R : Type ?u.7561} β R β [inst : IntegralDomain R] β Type ?u.7561p) :p: Rnav.nav: SurjVal pv (v: {R : Type ?u.7567} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβp ^p: Rn) = ofNn: ?m.7556n :=n: ?m.7556Goals accomplished! πend SurjVal structureGoals accomplished! πEnatValRing {EnatValRing: {R : Type u} β {p : R} β [inst : IntegralDomain R] β (valtn : SurjVal p) β (decr_val : R β R) β (β {x : R}, SurjVal.v valtn x = 0 β decr_val x = x) β (β {x : R}, SurjVal.v valtn x > 0 β x = p * decr_val x) β (residue_char : β) β (β (n : β), SurjVal.v valtn βn > 0 β residue_char β£ n) β (R β R) β (R β R β R β Bool) β EnatValRing pR :R: Type uType u} (Type u: Type (u + 1)p :p: RR) [R: Type uIntegralDomainIntegralDomain: Type ?u.8171 β Type ?u.8171R] whereR: Type uvaltn :valtn: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pSurjValSurjVal: {R : Type ?u.8176} β R β [inst : IntegralDomain R] β Type ?u.8176pp: Rdecr_val :decr_val: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β RR βR: Type uRR: Type uzero_valtn_decr {zero_valtn_decr: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : EnatValRing p) {x : R}, SurjVal.v self.valtn x = 0 β EnatValRing.decr_val self x = xx :x: RR} (h :R: Type uvaltn.valtn: SurjVal pvv: {R : Type ?u.8191} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx =x: R0) :0: ?m.8199decr_valdecr_val: R β Rx =x: Rxx: Rpos_valtn_decr {pos_valtn_decr: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : EnatValRing p) {x : R}, SurjVal.v self.valtn x > 0 β x = p * EnatValRing.decr_val self xx :x: RR} (h :R: Type uvaltn.valtn: SurjVal pvv: {R : Type ?u.8437} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx >x: R0) :0: ?m.8442x =x: Rp *p: Rdecr_valdecr_val: R β Rxx: Rresidue_char :residue_char: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β βββ: Typedef_char : βdef_char: β {R : Type u} {p : R} [inst : IntegralDomain R] (self : EnatValRing p) (n : β), SurjVal.v self.valtn βn > 0 β self.residue_char β£ nn :n: ββ,β: Typevaltn.valtn: SurjVal pv (v: {R : Type ?u.8567} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβn :n: βR) >R: Type u0 β0: ?m.8650residue_char β£residue_char: βnn: βnorm_repr :norm_repr: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β RR βR: Type uR --generalization of moduloR: Type uquad_roots_in_residue_field :quad_roots_in_residue_field: {R : Type u} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β R β R β BoolR βR: Type uR βR: Type uR βR: Type uBool namespace EnatValRing /-- reduce the element x by valuation n (by dividing by an appropriate power of the uniformizer) -/ defBool: Typesub_val {sub_val: {p : R} β EnatValRing p β R β β β Rp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.9675} β R β [inst : IntegralDomain R] β Type ?u.9675p) (p: Rx :x: RR) (R: Type un :n: ββ) :β: TypeR := matchR: Type un with |n: β0 =>0: βx | Nat.succx: Rn => matchn: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.9717} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.9724} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx with |x: R0 =>0: ββͺβx | _ =>x: Rsub_valsub_val: {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.9956} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx)x: Rn @[simp] lemman: βdecr_val_zero {decr_val_zero: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p), decr_val evr 0 = 0p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.10425} β R β [inst : IntegralDomain R] β Type ?u.10425p) :p: Revr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.10434} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β R0 =0: ?m.104420 :=0: ?m.10494
h
h
h
h
hGoals accomplished! π@[simp] lemma decr_val_neg {Goals accomplished! πp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.10798} β R β [inst : IntegralDomain R] β Type ?u.10798p) (p: Rx :x: RR) :R: Type uevr.evr: EnatValRing pdecr_val (-decr_val: {R : Type ?u.10809} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx) = -x: Revr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.10841} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx :=x: R
inl
inlGoals accomplished! π
inlGoals accomplished! π
inr
inrGoals accomplished! π
inr
inr@[simp] lemmaGoals accomplished! πdecr_val_p_mul {decr_val_p_mul: β {p : R} (evr : EnatValRing p) (x : R), decr_val evr (p * x) = xp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.11481} β R β [inst : IntegralDomain R] β Type ?u.11481p) (p: Rx :x: RR) :R: Type uevr.evr: EnatValRing pdecr_val (decr_val: {R : Type ?u.11492} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rp *p: Rx) =x: Rx :=x: RGoals accomplished! π@[simp] lemmaGoals accomplished! πsub_val_zero_n {sub_val_zero_n: β {p : R} (evr : EnatValRing p) (n : β), sub_val evr 0 n = 0p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.11932} β R β [inst : IntegralDomain R] β Type ?u.11932p) (p: Rn :n: ββ) :β: Typesub_valsub_val: {R : Type ?u.11943} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing p00: ?m.11954n =n: β0 :=0: ?m.12006
zeroGoals accomplished! π
succ@[simp] lemmaGoals accomplished! πsub_val_x_zero {sub_val_x_zero: β {p : R} (evr : EnatValRing p) (x : R), sub_val evr x 0 = xp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.13412} β R β [inst : IntegralDomain R] β Type ?u.13412p) (p: Rx :x: RR) :R: Type usub_valsub_val: {R : Type ?u.13423} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: R0 =0: ?m.13434x :=x: RlemmaGoals accomplished! πsub_val_val_zero {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.13493} β R β [inst : IntegralDomain R] β Type ?u.13493p) (p: Rx :x: RR) (R: Type um :m: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.13506} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.13513} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx =x: R0) :0: ?m.13521sub_valsub_val: {R : Type ?u.13753} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rm =m: βx :=x: R
zeroGoals accomplished! π
succlemmaGoals accomplished! πsub_val_val_pos_succ {sub_val_val_pos_succ: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) (x : R) (m : β), SurjVal.v evr.valtn x β 0 β sub_val evr x (Nat.succ m) = sub_val evr (decr_val evr x) mp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.14381} β R β [inst : IntegralDomain R] β Type ?u.14381p) (p: Rx :x: RR) (R: Type um :m: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.14395} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.14402} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx βx: R0) :0: ?m.14410sub_valsub_val: {R : Type ?u.14628} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing px (Nat.succx: Rm) =m: βsub_valsub_val: {R : Type ?u.14635} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.14642} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx)x: Rm :=m: βlemmaGoals accomplished! πval_decr_val {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.16342} β R β [inst : IntegralDomain R] β Type ?u.16342p) (p: Rx :x: RR) (h :R: Type uevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.16350} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.16354} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx = ofNx: Rm) :m: ?m.16337evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.16362} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.16366} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.16370} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx) = ofN (x: Rm -m: ?m.163371) :=1: ?m.16378R: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)R: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)R: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)lemmaGoals accomplished! πsub_val_decr_val_comm {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.16792} β R β [inst : IntegralDomain R] β Type ?u.16792p) (p: Rx :x: RR) (R: Type un :n: ββ) :β: Typesub_valsub_val: {R : Type ?u.16805} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pevr.evr: EnatValRing pdecr_valdecr_val: {R : Type ?u.16815} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rx)x: Rn =n: βevr.evr: EnatValRing pdecr_val (decr_val: {R : Type ?u.16819} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β R β Rsub_valsub_val: {R : Type ?u.16823} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn) :=n: β
zeroGoals accomplished! πGoals accomplished! πGoals accomplished! πGoals accomplished! πlemmaGoals accomplished! πval_sub_val_eq {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.17734} β R β [inst : IntegralDomain R] β Type ?u.17734p) (p: Rx :x: RR) (R: Type un :n: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.17744} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.17748} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx = ofNx: Rm) :m: ?m.17729evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.17756} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.17760} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβsub_valsub_val: {R : Type ?u.17764} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn) = ofN (n: βm -m: ?m.17729n) :=n: β
zero
zeroGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n, m: β
h: SurjVal.v evr.valtn x = ofN (Nat.succ m)
ih: SurjVal.v evr.valtn (sub_val evr x n) = ofN (Nat.succ m - n)
succ.succ.hGoals accomplished! πlemmaGoals accomplished! πval_sub_val_le {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.18472} β R β [inst : IntegralDomain R] β Type ?u.18472p) (p: Rx :x: RR) (R: Type un :n: ββ) (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.18482} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.18486} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rm) :m: ?m.18467evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.18498} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.18502} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβsub_valsub_val: {R : Type ?u.18506} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn) β₯ ofN (n: βm -m: ?m.18467n) :=n: βGoals accomplished! πGoals accomplished! πlemmaGoals accomplished! πfactor_p_of_le_val {factor_p_of_le_val: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) {x : R} {n : β}, SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x np :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.19029} β R β [inst : IntegralDomain R] β Type ?u.19029p) {p: Rx :x: RR} {R: Type un :n: ββ} (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.19042} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.19049} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) :n: βx =x: Rp ^p: Rn *n: βsub_valsub_val: {R : Type ?u.19070} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn :=n: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
h: SurjVal.v evr.valtn x β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
h: SurjVal.v evr.valtn x β₯ ofN nGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
h: SurjVal.v evr.valtn x β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
pos_val: SurjVal.v evr.valtn (sub_val evr x n) > 0
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
ih: SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x n
h: SurjVal.v evr.valtn x β₯ ofN (Nat.succ n)
succ.hlemmaGoals accomplished! πfactor_p_of_eq_val {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.20229} β R β [inst : IntegralDomain R] β Type ?u.20229p) {p: Rx :x: RR} {R: Type un :n: ββ} (h :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.20242} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.20249} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx = ofNx: Rn) :n: βx =x: Rp ^p: Rn *n: βsub_valsub_val: {R : Type ?u.20266} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn :=n: βfactor_p_of_le_valfactor_p_of_le_val: β {R : Type ?u.20486} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) {x : R} {n : β}, SurjVal.v evr.valtn x β₯ ofN n β x = p ^ n * sub_val evr x nevr (le_of_eq (Eq.symm h)) lemma sub_val_p_mul {evr: EnatValRing pp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.20549} β R β [inst : IntegralDomain R] β Type ?u.20549p) (p: Rx :x: RR) (R: Type un :n: ββ) :β: Typesub_valsub_val: {R : Type ?u.20562} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing pp ^p: Rn *n: βx)x: Rn =n: βx :=x: R
zero
zero
zero
zero
zero
zero
zeroGoals accomplished! π
succ
succ.h
succ
succ.h
succ
succ.hlemmaGoals accomplished! πsub_val_neg {sub_val_neg: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) {x : R} {n : β}, sub_val evr (-x) n = -sub_val evr x np :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.21467} β R β [inst : IntegralDomain R] β Type ?u.21467p) {p: Rx :x: RR} {R: Type un :n: ββ} :β: Typesub_valsub_val: {R : Type ?u.21480} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (-evr: EnatValRing px)x: Rn = -n: βsub_valsub_val: {R : Type ?u.21515} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn :=n: β
zeroGoals accomplished! πGoals accomplished! πGoals accomplished! πGoals accomplished! πlemmaGoals accomplished! πsub_val_add {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.22264} β R β [inst : IntegralDomain R] β Type ?u.22264p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.22279} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.22286} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.22301} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.22305} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rn) :n: βsub_valsub_val: {R : Type ?u.22314} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px +x: Ry)y: Rn =n: βsub_valsub_val: {R : Type ?u.22421} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn +n: βsub_valsub_val: {R : Type ?u.22428} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rn :=n: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nlemmaGoals accomplished! πsub_val_sub {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.22932} β R β [inst : IntegralDomain R] β Type ?u.22932p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.22947} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.22954} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.22969} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.22973} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rn) :n: βsub_valsub_val: {R : Type ?u.22982} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px -x: Ry)y: Rn =n: βsub_valsub_val: {R : Type ?u.23053} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn -n: βsub_valsub_val: {R : Type ?u.23060} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rn :=n: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN nlemmaGoals accomplished! πsub_val_mul_left {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.23625} β R β [inst : IntegralDomain R] β Type ?u.23625p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.23640} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.23647} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) :n: βsub_valsub_val: {R : Type ?u.23662} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry)y: Rn =n: βsub_valsub_val: {R : Type ?u.23765} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn *n: βy :=y: RR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
aGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
aR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN nR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN nlemmaGoals accomplished! πsub_val_mul_right {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.24269} β R β [inst : IntegralDomain R] β Type ?u.24269p) {p: Rxx: Ry :y: RR} {R: Type un :n: ββ} (hy :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.24284} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.24291} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rn) :n: βsub_valsub_val: {R : Type ?u.24306} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry)y: Rn =n: βx *x: Rsub_valsub_val: {R : Type ?u.24409} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rn :=n: βlemmaGoals accomplished! πsub_val_mul_sub_val {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.24592} β R β [inst : IntegralDomain R] β Type ?u.24592p) {p: Rxx: Ry :y: RR} (R: Type unn: βm :m: ββ) (hx :β: Typeevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.24609} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.24616} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.24631} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.24635} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rm) :m: βsub_valsub_val: {R : Type ?u.24647} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn *n: βsub_valsub_val: {R : Type ?u.24654} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rm =m: βsub_valsub_val: {R : Type ?u.24661} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry) (y: Rn +n: βm) :=m: βR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x, y: R
n, m: β
hx: SurjVal.v evr.valtn x β₯ ofN n
hy: SurjVal.v evr.valtn y β₯ ofN mGoals accomplished! πlemmaGoals accomplished! πsub_val_mul {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.25874} β R β [inst : IntegralDomain R] β Type ?u.25874p) {p: Rxx: Ry :y: RR} (R: Type unn: βm :m: ββ) {β: Typenm :nm: ββ} (h :β: Typen +n: βm =m: βnm) (hx :nm: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.25937} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.25944} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) (hy :n: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.25959} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.25963} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβy β₯ ofNy: Rm) :m: βsub_valsub_val: {R : Type ?u.25972} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px *x: Ry)y: Rnm =nm: βsub_valsub_val: {R : Type ?u.26075} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn *n: βsub_valsub_val: {R : Type ?u.26082} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pyy: Rm :=m: βlemmaGoals accomplished! πsub_val_pow {p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.26211} β R β [inst : IntegralDomain R] β Type ?u.26211p) {p: Rx :x: RR} (R: Type unn: βk :k: ββ) {β: Typenm :nm: ββ} (h :β: Typek *k: βn =n: βnm) (hx :nm: βevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.26276} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.26283} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβx β₯ ofNx: Rn) :n: βsub_valsub_val: {R : Type ?u.26298} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing px ^x: Rk)k: βnm =nm: βsub_valsub_val: {R : Type ?u.26438} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rn ^n: βk :=k: βGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nmR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hyR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hxR: Type u
instβ: IntegralDomain R
p: R
evr: EnatValRing p
x: R
n: β
hx: SurjVal.v evr.valtn x β₯ ofN n
k: β
ih: β {nm : β}, k * n = nm β sub_val evr (x ^ k) nm = sub_val evr x n ^ k
nm: β
h: Nat.succ k * n = nm
succ.hylemmaGoals accomplished! πsub_val_sub_val {sub_val_sub_val: β {R : Type u} [inst : IntegralDomain R] {p : R} (evr : EnatValRing p) {x : R} {m n : β}, sub_val evr (sub_val evr x m) n = sub_val evr x (m + n)p :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.27271} β R β [inst : IntegralDomain R] β Type ?u.27271p) {p: Rx :x: RR} {R: Type umm: βn :n: ββ} :β: Typesub_valsub_val: {R : Type ?u.27286} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revr (evr: EnatValRing psub_valsub_val: {R : Type ?u.27296} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing pxx: Rm)m: βn =n: βsub_valsub_val: {R : Type ?u.27300} β [inst : IntegralDomain R] β {p : R} β EnatValRing p β R β β β Revrevr: EnatValRing px (x: Rm +m: βn) :=n: β
zeroGoals accomplished! πGoals accomplished! πGoals accomplished! πdefGoals accomplished! πhas_double_root {has_double_root: {p : R} β (evr : EnatValRing p) β (a b c : R) β ?m.27986 evr a b cp :p: RR} (R: Type uevr :evr: EnatValRing pEnatValRingEnatValRing: {R : Type ?u.27971} β R β [inst : IntegralDomain R] β Type ?u.27971p) (p: Raa: Rbb: Rc :c: RR) :=R: Type uevr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.28007} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pvv: {R : Type ?u.28011} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβa =a: R0 β§0: ?m.28019evr.evr: EnatValRing pvaltn.valtn: {R : Type ?u.28249} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv (v: {R : Type ?u.28253} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβb ^b: R2 -2: ?m.282644 *4: ?m.28280a *a: Rc) >c: R0 end EnatValRing def0: ?m.28593nat_prime (nat_prime: β β Propp :p: ββ) :β: TypeProp :=Prop: Type1 <1: ?m.28888p β§ (βp: βaa: βb :b: ββ, (β: Typea *a: βb) %b: βp =p: β0 β0: ?m.28935a %a: βp =p: β0 β¨0: ?m.29033b %b: βp =p: β0) lemma ndiv_mul_left (0: ?m.29072aa: βbb: βp :p: ββ) : (β: Typea *a: βb) %b: βp βp: β0 β0: ?m.29211a %a: βp βp: β0 :=0: ?m.29246lemma ndiv_mul_right (Goals accomplished! πaa: βbb: βp :p: ββ) : (β: Typea *a: βb) %b: βp βp: β0 β0: ?m.29510b %b: βp βp: β0 :=0: ?m.29545lemmaGoals accomplished! πnat_prime_test (p :p: ββ) :β: Typenat_primenat_prime: β β Propp β (p: β1 <1: ?m.29598p β§ (βp: βaa: βb :b: ββ,β: Typea <a: βp βp: βb <b: βp β (p: βa *a: βb) %b: βp =p: β0 β0: ?m.29655a %a: βp =p: β0 β¨0: ?m.29753b %b: βp =p: β0)) :=0: ?m.29792
mp
mpr
mp
mpr
mp
mpr
mp
mpr
mp
mprGoals accomplished! π:Goals accomplished! πDecidablePred (DecidablePred: {Ξ± : Sort ?u.30118} β (Ξ± β Prop) β Sort (max 1 ?u.30118)nat_prime . :nat_prime: β β Propβ ββ: TypeProp) := funProp: Typep =>p: ?m.30132sorry --match p with --| 0 => sorry --isFalse (not_and_of_not_left _ (not_lt_of_ge (le_of_lt Nat.zero_lt_one))) --| 1 => isFalse (not_and_of_not_left _ (not_lt_of_ge (le_of_eq rfl))) --| Nat.succ (Nat.succ p') => sorry --def fmul_eq_addf {R R' : Type u} [Mul R] [Add R'] (f : R β R') (x y : R) : Prop := f (x * y) = f x + f y namespace Int def nat_valuation :sorry: ?m.30135β ββ: Typeβ ββ: Typeββͺβ | _,ββͺβ: Type0 =>0: ββ |β: ββͺβ0, (0: β_+1) => ofN_: β0 |0: ?m.302861, (1: β_+1) =>_: ββ | (β: ββͺβq+2), (q: βm+1) => if (m: βm+m: β1) % (1: ?m.30467q+q: β2) β2: ?m.304810 then ofN0: ?m.305730 else succ (nat_valuation (0: ?m.30580q+q: β2) ((2: ?m.30586m+m: β1) / (1: ?m.30631q+q: β2))) termination_by nat_valuation p k =>2: ?m.30645k decreasing_byk: βlemmaGoals accomplished! πnat_val_zero (nat_val_zero: β (p : β), nat_valuation p 0 = βp :p: ββ) : nat_valuationβ: Typepp: β0 =0: ?m.32225β :=β: ββͺβnat_valuation p 0 = βlemmaGoals accomplished! πnat_val_succ (qq: βm :m: ββ) : nat_valuation (β: Typeq+q: β2) (2: ?m.45419m+m: β1) = if (1: ?m.45473m+m: β1) % (1: ?m.45534q+q: β2) β2: ?m.455480 then ofN0: ?m.456400 else succ (nat_valuation (0: ?m.45651q+q: β2) ((2: ?m.45657m+m: β1) / (1: ?m.45702q+q: β2))) :=2: ?m.45716def int_val (Goals accomplished! πp :p: ββ) (β: Typek :k: β€β€) :β€: Typeββͺβ := nat_valuationββͺβ: Typep (natAbsp: βk) lemma int_val_uniformizer {k: β€p :p: ββ} (β: Typegt1 :gt1: 1 < p1 <1: ?m.48737p) : int_valp: βpp: βp = ofNp: β1 :=1: ?m.48859nat_valuation p p = ofN 1nat_valuation p p = ofN 1nat_valuation 0 0 = ofN 1nat_valuation p p = ofN 1
hnat_valuation 0 0 = ofN 1
h1 < 0nat_valuation 0 0 = ofN 1Goals accomplished! πnat_valuation p p = ofN 1nat_valuation (Nat.succ 0) (Nat.succ 0) = ofN 1nat_valuation p p = ofN 1
hnat_valuation (Nat.succ 0) (Nat.succ 0) = ofN 1
h1 < 1nat_valuation (Nat.succ 0) (Nat.succ 0) = ofN 1Goals accomplished! πnat_valuation p p = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation p p = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1
hc
hcnat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1nat_valuation (q + 2) (q + 2) = ofN 1lemmaGoals accomplished! πnat_val_mul_eq_add (nat_val_mul_eq_add: β (p : β), nat_prime p β β (a b : β), nat_valuation p (a * b) = nat_valuation p a + nat_valuation p bp :p: ββ) (β: Typeprime :prime: nat_prime pnat_primenat_prime: β β Propp) (p: βaa: βb :b: ββ) : nat_valuationβ: Typep (p: βa *a: βb) = nat_valuationb: βpp: βa + nat_valuationa: βpp: βb :=b: βnat_valuation p (a * b) = nat_valuation p a + nat_valuation p bnat_valuation p (a * b) = nat_valuation p a + nat_valuation p bβ (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dβ (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeroβ (c d : β), c + d β€ Nat.zero β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeroβ (c d : β), c + d β€ Nat.zero β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (0 * d) = nat_valuation p 0 + nat_valuation p d
zeronat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
zeronat_valuation p (0 * 0) = nat_valuation p 0 + nat_valuation p 0
zeronat_valuation p (0 * 0) = nat_valuation p 0 + nat_valuation p 0
zeroβ (c d : β), c + d β€ Nat.zero β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dGoals accomplished! πβ (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
succβ (c d : β), c + d β€ Nat.succ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: c + d β€ Nat.succ n
succnat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
succβ (c d : β), c + d β€ Nat.succ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: c + d β€ Nat.succ n
succnat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d: β
h_sum: Nat.zero + d β€ Nat.succ n
succ.zeronat_valuation p (Nat.zero * d) = nat_valuation p Nat.zero + nat_valuation p dGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: c + d β€ Nat.succ n
succnat_valuation p (c * d) = nat_valuation p c + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d, c: β
h_sum: Nat.succ c + d β€ Nat.succ n
succ.succnat_valuation p (Nat.succ c * d) = nat_valuation p (Nat.succ c) + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d, c: β
h_sum: Nat.succ c + d β€ Nat.succ n
succ.succnat_valuation p (Nat.succ c * d) = nat_valuation p (Nat.succ c) + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c: β
h_sum: Nat.succ c + Nat.zero β€ Nat.succ n
succ.succ.zeronat_valuation p (Nat.succ c * Nat.zero) = nat_valuation p (Nat.succ c) + nat_valuation p Nat.zeroGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
d, c: β
h_sum: Nat.succ c + d β€ Nat.succ n
succ.succnat_valuation p (Nat.succ c * d) = nat_valuation p (Nat.succ c) + nat_valuation p dR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
succ.succ.succnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
succ.succ.succnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
succ.succ.succnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: 2 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p(if (c * d + c + d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c * d + c + d + 1) / (q + 2)))) = (if (c + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c + 1) / (q + 2)))) + if (d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((d + 1) / (q + 2)))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p(if (c * d + c + d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c * d + c + d + 1) / (q + 2)))) = (if (c + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((c + 1) / (q + 2)))) + if (d + 1) % (q + 2) β 0 then ofN 0 else succ (nat_valuation (q + 2) ((d + 1) / (q + 2)))Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: Nat.succ 1 + q = pnat_valuation p (Nat.succ c * Nat.succ d) = nat_valuation p (Nat.succ c) + nat_valuation p (Nat.succ d)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
xβ: (c + 1) * (d + 1) % p = 0 β¨ (c + 1) * (d + 1) % p > 0R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
xβ: (c + 1) % p = 0 β¨ (d + 1) % p = 0
inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p)) + nat_valuation p (d + 1)R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p ((c + 1) / p) + nat_valuation p (d + 1))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ nGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) / p * (d + 1)
inl.inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (c + 1) % p = 0
sum_le_n: (c + 1) / p + (d + 1) β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) / p * (d + 1)
inl.inlGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
xβ: (c + 1) % p = 0 β¨ (d + 1) % p = 0
inlR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = nat_valuation p (c + 1) + succ (nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))Goals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrsucc (nat_valuation p ((c + 1) * (d + 1) / p)) = succ (nat_valuation p (c + 1) + nat_valuation p ((d + 1) / p))R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ nGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) * ((d + 1) / p)
inl.inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p = 0
h': (d + 1) % p = 0
sum_le_n: c + 1 + (d + 1) / p β€ n
mul_div_assoc: (c + 1) * (d + 1) / p = (c + 1) * ((d + 1) / p)
inl.inrGoals accomplished! πR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
xβ: (c + 1) * (d + 1) % p = 0 β¨ (c + 1) * (d + 1) % p > 0R: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrR: Type u
instβ: IntegralDomain R
p: β
prime: nat_prime p
a, b, n: β
ih: β (c d : β), c + d β€ n β nat_valuation p (c * d) = nat_valuation p c + nat_valuation p d
c, d: β
h_sum: Nat.succ c + Nat.succ d β€ Nat.succ n
q: β
hq: q + 2 = p
h: (c + 1) * (d + 1) % p > 0
hc: (c + 1) % p β 0
hd: (d + 1) % p β 0
inrGoals accomplished! πnat_valuation p (a * b) = nat_valuation p a + nat_valuation p blemmaGoals accomplished! πint_val_mul_eq_add (p :p: ββ) (β: Typeprime :prime: nat_prime pnat_primenat_prime: β β Propp) (p: βaa: β€b :b: β€β€) : int_valβ€: Typep (p: βa *a: β€b) = int_valb: β€pp: βa + int_vala: β€pp: βb :=b: β€nat_valuation p (natAbs a * natAbs b) = nat_valuation p (natAbs a) + nat_valuation p (natAbs b)lemma (Goals accomplished! πpp: βaa: βb :b: ββ) : nat_valuationβ: Typep (p: βa +a: βb) β₯b: βmin (nat_valuationmin: {Ξ± : Type ?u.54447} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±pp: βa) (nat_valuationa: βpp: βb) :=b: βnat_valuation p (a + b) β₯ min (nat_valuation p a) (nat_valuation p b)lemma (Goals accomplished! πaa: β€b :b: β€β€) : natAbs (β€: Typea +a: β€b) =b: β€max (natAbsmax: {Ξ± : Type ?u.54532} β [self : Max Ξ±] β Ξ± β Ξ± β Ξ±a) (natAbsa: β€b) -b: β€min (natAbsmin: {Ξ± : Type ?u.54538} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±a) (natAbsa: β€b) :=b: β€lemma (Goals accomplished! πp :p: ββ) (β: Typeaa: β€b :b: β€β€) : int_valβ€: Typep (p: βa +a: β€b) β₯b: β€min (int_valmin: {Ξ± : Type ?u.54644} β [self : Min Ξ±] β Ξ± β Ξ± β Ξ±pp: βa) (int_vala: β€pp: βb) :=b: β€nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)) β₯ min (nat_valuation p (natAbs a)) (nat_valuation p (natAbs b))lemma (Goals accomplished! πp :p: ββ) (β: Typeaa: β€b :b: β€β€) (h : int_valβ€: Typepp: βa < int_vala: β€pp: βb) : int_valb: β€p (p: βa +a: β€b) = int_valb: β€pp: βa :=a: β€lemma (Goals accomplished! πp :p: ββ) (β: Typegt1 :gt1: 1 < p1 <1: ?m.54986p) (p: βa :a: β€β€) : int_valβ€: Typepp: βa =a: β€β ββ: ββͺβa =a: β€0 :=0: ?m.55027def primeVal {Goals accomplished! πp :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) :p: βSurjVal (ofNatSurjVal: {R : Type ?u.55068} β R β [inst : IntegralDomain R] β Type ?u.55068p) := { v := int_valp: βp, v_uniformizer := int_val_uniformizerp: βhp.hp: nat_prime pleft, v_mul_eq_add_v := int_val_mul_eq_addleft: β {a b : Prop}, a β§ b β app: βhp, v_add_ge_min_v := int_val_add_ge_minhp: nat_prime pp, v_eq_top_iff_zero := int_val_eq_top_iff_zerop: βpp: βhp.hp: nat_prime pleft } def decr_val_p (left: β {a b : Prop}, a β§ b β ap :p: ββ) (val :β: Typeβ€ ββ€: Typeββͺβ) (ββͺβ: Typek :k: β€β€) :β€: Typeβ€ := match valβ€: Typek with |k: β€0 =>0: ββͺβk | _ =>k: β€k /k: β€p lemmap: βzero_valtn_decr_p {p:p: ββ} {β: Typek :k: β€β€} (val :β€: Typeβ€ ββ€: Typeββͺβ) (ββͺβ: Typeh : valh: val k = 0k =k: β€0) : decr_val_p0: ?m.55869p valp: βk =k: β€k :=k: β€decr_val_p p val k = kdecr_val_p p val k = kdecr_val_p p val k = kdef norm_repr_p (Goals accomplished! πp :p: ββ) (β: Typex :x: β€β€) :β€: Typeβ€ := (β€: Typex % (x: β€p :p: ββ€) +β€: Typep) % (p: βp :p: ββ€) lemma (β€: Typep :p: ββ) : ββ: Typen :n: ββ, (primeValβ: Typehp).hp: ?m.56470vv: {R : Type ?u.56482} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβn >n: β0 β0: ?m.56578p β£p: βn :=n: βsorry def {sorry: ?m.56810p :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) :p: βEnatValRing (EnatValRing: {R : Type ?u.56827} β R β [inst : IntegralDomain R] β Type ?u.56827p :p: ββ€) := { valtn := primeValβ€: Typehp, decr_val := decr_val_php: nat_prime pp (primeValp: βhp).hp: nat_prime pv, zero_valtn_decr := zero_valtn_decr_p (primeValv: {R : Type ?u.56938} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβhp).hp: nat_prime pv, pos_valtn_decr :=v: {R : Type ?u.56952} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβsorry, residue_char :=sorry: ?m.56979p, def_char := def_char_pp: βp, norm_repr := norm_repr_pp: βp, quad_roots_in_residue_field := funp: βaa: ?m.58104bb: ?m.58107c => Int.quad_root_in_ZpZc: ?m.58110aa: ?m.58104bb: ?m.58107cc: ?m.58110p } lemma :p: βnat_primenat_prime: β β Prop2 :=2: ?m.58359lemma :Goals accomplished! πnat_primenat_prime: β β Prop3 :=3: ?m.58569def modulo (Goals accomplished! πx :x: β€β€) (β€: Typep :p: ββ) := (β: Typex % (x: β€p:p: ββ€) +β€: Typep) % (p: βp:p: ββ€) def inv_mod (β€: Typex :x: β€β€) (β€: Typep :p: ββ) := modulo (β: Typex ^ (x: β€p -p: β2))2: ?m.59101p def has_double_root (p: βaa: β€bb: β€c :c: β€β€) {β€: Typep :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) := letp: βv_p := (v_p: ?m.59379primeEVRprimeEVR: {p : β} β nat_prime p β EnatValRing βphp).hp: nat_prime pvaltn.valtn: {R : Type ?u.59382} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv;v: {R : Type ?u.59392} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβv_pv_p: ?m.59379a =a: β€0 β§0: ?m.59415v_p (v_p: ?m.59379b ^b: β€2 -2: ?m.596514 *4: ?m.59667a *a: β€c) >c: β€0 def double_root (0: ?m.59888aa: β€bb: β€c :c: β€β€) (β€: Typep :p: ββ) := ifβ: Typep =p: β2 then modulo2: ?m.60166cc: β€2 else modulo (-2: ?m.60200b * inv_mod (b: β€2 *2: ?m.60210a)a: β€p)p: βp lemma {p: βp :p: ββ} (β: Typehp :hp: nat_prime pnat_primenat_prime: β β Propp) (p: βaa: β€bb: β€c :c: β€β€) (β€: TypeH : has_double_rootH: has_double_root a b c hpaa: β€bb: β€cc: β€hp) : lethp: nat_prime px := double_rootx: ?m.60429aa: β€bb: β€cc: β€p; letp: βv_p := (v_p: ?m.60432primeEVRprimeEVR: {p : β} β nat_prime p β EnatValRing βphp).hp: nat_prime pvaltn.valtn: {R : Type ?u.60434} β {p : R} β [inst : IntegralDomain R] β EnatValRing p β SurjVal pv;v: {R : Type ?u.60444} β {p : R} β [inst : IntegralDomain R] β SurjVal p β R β ββͺβv_p (v_p: ?m.60432a*a: β€x^x: ?m.604292 +2: ?m.60469b*b: β€x +x: ?m.60429c) >c: β€0 β§0: ?m.60696v_p (v_p: ?m.604322*2: ?m.61008a*a: β€x +x: ?m.60429b) >b: β€0 :=0: ?m.61092end IntGoals accomplished! π